// Copyright 2019 - University of Strathclyde, King's College London and Schlumberger Ltd
// This source code is licensed under the BSD license found in the LICENSE file in the root directory of this source tree.

#include "Environment.h"
#include "Ownership.h"
#include "Polynomial.h"
#include "ptree.h"
#include <iostream>
#include <set>

#ifndef __PROPOSITION
#define __PROPOSITION

//#define map std::map
//#define vector std::vector

using std::map;
using std::set;
using std::vector;

namespace VAL {

  class State;
  class Action;

  struct ActiveCtsEffects;
  class DerivedGoal;
  class AdviceProposition;

  bool isPointInInterval(
      CoScalar p, const vector< pair< intervalEnd, intervalEnd > > &ints);
  bool isPointInInterval(CoScalar p,
                         const pair< intervalEnd, intervalEnd > &ints);
  bool isPointInInterval(CoScalar p,
                         const vector< pair< intervalEnd, intervalEnd > > &ints,
                         const pair< intervalEnd, intervalEnd > &int1);
  pair< intervalEnd, intervalEnd > getIntervalFromPt(
      intervalEnd p, const vector< pair< intervalEnd, intervalEnd > > &ints,
      const pair< intervalEnd, intervalEnd > &int1);

  Intervals setIntersect(const Intervals &ints1, const Intervals &ints2);
  Intervals setUnion(const Intervals &ints1, const Intervals &ints2);
  Intervals setComplement(const Intervals &ints, double endPoint);

  class Proposition {
   protected:
    const Environment &bindings;
    double endOfInterval;

   public:
    virtual ~Proposition(){};
    Proposition(const Environment &bs) : bindings(bs), endOfInterval(0){};
    virtual pair< int, int > rank() const = 0;
    virtual bool evaluate(const State *s,
                          vector< const DerivedGoal * > =
                              vector< const DerivedGoal * >()) const = 0;
    virtual Intervals getIntervals(const State *s) const = 0;
    virtual string getPropString(const State *s) const = 0;
    virtual set< const SimpleProposition * > getLiterals() const = 0;
    virtual const AdviceProposition *getAdviceProp(const State *s) const;
    virtual const AdviceProposition *getAdviceNegProp(const State *s) const;
    virtual bool markOwnedPreconditions(const Action *a, Ownership &o,
                                        ownership w) const = 0;

    virtual void setUpComparisons(const ActiveCtsEffects *ace,
                                  bool rhsOpen = false) = 0;
    virtual void resetCtsFunctions() = 0;
    virtual bool evaluateAtPointWithinError(
        const State *s,
        vector< const DerivedGoal * > = vector< const DerivedGoal * >()) const;
    double getEndOfInterval() const { return endOfInterval; };
    bool markOwnedPreconditions(const Action *a, Ownership &o) const {
      return markOwnedPreconditions(a, o, E_PPRE);
    };
    virtual void write(ostream &o) const { o << "Compound proposition..."; };

    virtual void destroy() const { delete this; };
  };

  ostream &operator<<(ostream &o, const Proposition &p);

  class SimpleProposition : public Proposition {
   private:
    static Environment nullEnvironment;

    const proposition *prop;

   public:
    SimpleProposition(const parse_category *p, const Environment &bs)
        : Proposition(bs), prop(dynamic_cast< const proposition * >(p)){};
    SimpleProposition(const parse_category *p)
        : Proposition(nullEnvironment),
          prop(dynamic_cast< const proposition * >(p)){};

    bool evaluate(const State *s, vector< const DerivedGoal * > =
                                      vector< const DerivedGoal * >()) const;

    ~SimpleProposition(){};

    Intervals getIntervals(const State *s) const;
    string getPropString(const State *s) const;
    string getPropName() const { return prop->head->getName(); };
    string getParameter(int paraNo) const;
    const AdviceProposition *getAdviceProp(const State *s) const;
    const AdviceProposition *getAdviceNegProp(const State *s) const;
    set< const SimpleProposition * > getLiterals() const;
    const_symbol_list *getConstants(var_symbol_list *variables,
                                    parameter_symbol_list *psl,
                                    Validator *vld) const;
    bool checkParametersConstantsMatch(parameter_symbol_list *psl) const;
    bool checkConstantsMatch(parameter_symbol_list *psl) const;
    pair< int, int > rank() const;
    bool markOwnedPreconditions(const Action *a, Ownership &o,
                                ownership w) const;
    void setUpComparisons(const ActiveCtsEffects *ace, bool rhsOpen = false);
    void resetCtsFunctions();

    const pred_symbol *getPred() const { return prop->head; };
    const proposition *getProp() const { return prop; };
    const Environment *getEnv() const { return &bindings; };
    void write(ostream &o) const;
    string toString() const;
    void destroy() const {};
  };

  class DerivedGoal : public Proposition {
   private:
    static Environment nullEnvironment;

    const proposition *prop;

    const Proposition *deriveFormula;
    mutable bool revisit;

    static map< string, bool > DPliterals;
    static vector< string > calledDPsEval;
    static map< string, pair< int, int > > ranks;
    static const pair< int, int > noRank;
    static map< string, bool > evals;
    static const int noEval;
    static map< string, Intervals > intervals;
    static const Intervals noIntervals;
    static map< string, string > propStrings;
    static const string noPropString;
    static map< string, const Action * > preCons;
    static const ActiveCtsEffects *ace;
    static bool rhsOpen;

   public:
    DerivedGoal(const parse_category *p, const Proposition *f,
                const Environment &bs)
        : Proposition(bs),
          prop(dynamic_cast< const proposition * >(p)),
          deriveFormula(f),
          revisit(false){};
    DerivedGoal(const parse_category *p, const Proposition *f)
        : Proposition(nullEnvironment),
          prop(dynamic_cast< const proposition * >(p)),
          deriveFormula(f),
          revisit(false){};

    bool evaluate(const State *s, vector< const DerivedGoal * > =
                                      vector< const DerivedGoal * >()) const;
    Intervals getIntervals(const State *s) const;
    string getPropString(const State *s) const;
    set< const SimpleProposition * > getLiterals() const;
    pair< int, int > rank() const;
    const AdviceProposition *getAdviceProp(const State *s) const;
    const AdviceProposition *getAdviceNegProp(const State *s) const;
    bool markOwnedPreconditions(const Action *a, Ownership &o,
                                ownership w) const;
    void setUpComparisons(const ActiveCtsEffects *ace, bool rhsOpen = false);
    void resetCtsFunctions();

    void removeCalledDP(string dp) const;
    void addCalledDP(string dp) const;
    string getDPName() const;
    bool visited() const;
    bool visited(string dp) const;
    void setRevisit(bool b) const { revisit = b; };
    static void resetLists(const State *s);
    static void resetPreConsList() { preCons.clear(); };

    static void setACE(const ActiveCtsEffects *a, bool r) {
      ace = a;
      rhsOpen = r;
    };

    void write(ostream &o) const;

    ~DerivedGoal() { deriveFormula->destroy(); };
  };

  // used when creating a derived predicate that may depend on itself
  class FalseProposition : public Proposition {
   private:
    bool trueProp;

   public:
    FalseProposition(const Environment &bs, bool tp = false)
        : Proposition(bs), trueProp(tp){};

    bool evaluate(const State *s, vector< const DerivedGoal * > =
                                      vector< const DerivedGoal * >()) const;
    Intervals getIntervals(const State *s) const {
      Intervals theAns;
      return theAns;
    };
    string getPropString(const State *s) const {
      if (trueProp)
        return "true";
      else
        return "false";
    };
    set< const SimpleProposition * > getLiterals() const {
      return set< const SimpleProposition * >();
    };
    pair< int, int > rank() const { return make_pair(0, 0); };
    bool markOwnedPreconditions(const Action *a, Ownership &o,
                                ownership w) const;
    void setUpComparisons(const ActiveCtsEffects *ace, bool rhsOpen = false) {
      return;
    };
    void resetCtsFunctions() { return; };
    void write(ostream &o) const {
      if (trueProp)
        o << "(TRUE)";
      else
        o << "(FALSE)";
    };
  };

  class Comparison : public Proposition {
   private:
    const comparison *comp;
    const CtsFunction *ctsFtn;
    bool rhsIntervalOpen;  // only open for last interval that invariant is
                           // checked on
   public:
    Comparison(const comparison *c, const Environment &bs)
        :

          Proposition(bs),
          comp(c),
          ctsFtn(0){};
    bool evaluate(const State *s, vector< const DerivedGoal * > =
                                      vector< const DerivedGoal * >()) const;
    bool evaluateAtPoint(const State *s) const;
    bool evaluateAtPointError(const State *s) const;
    bool evaluateAtPointWithinError(
        const State *s,
        vector< const DerivedGoal * > = vector< const DerivedGoal * >()) const;
    Intervals getIntervals(const State *s) const;

    const comparison *getComparison() const { return comp; };
    string getPropString(const State *s) const;
    string getPropAdviceString(const State *s) const;
    string getExprnString(const expression *e, const Environment &bs,
                          const State *s) const;
    string getExprnString(const expression *e, const Environment &bs) const;
    set< const SimpleProposition * > getLiterals() const;
    pair< int, int > rank() const;
    // first value, no comparison with changing fe s, send rank - max degree of
    // polys for in condition
    bool markOwnedPreconditions(const Action *a, Ownership &o,
                                ownership w) const;
    void setUpComparisons(const ActiveCtsEffects *ace, bool rhsOpen = false);
    void resetCtsFunctions();
    const AdviceProposition *getAdviceProp(const State *s) const;
    const AdviceProposition *getAdviceNegProp(const State *s) const;
    vector< CoScalar > getRoots(const State *s, CoScalar t) const;
    vector< CoScalar > getRootsForIntervals(const State *s, CoScalar t) const;
    void write(ostream &o) const;

    // void destroy() {/*delete this;*/};
    ~Comparison() { /*cout<<"deleting "<<*ctsFtn<<"\n";*/
      delete ctsFtn;
    };
  };

  class ConjGoal : public Proposition {
   private:
    const vector< const Proposition * > gs;

   public:
    ConjGoal(const conj_goal *c, const vector< const Proposition * > &g,
             const Environment &bs)
        : Proposition(bs), gs(g){};
    bool evaluate(const State *, vector< const DerivedGoal * > =
                                     vector< const DerivedGoal * >()) const;
    Intervals getIntervals(const State *s) const;
    string getPropString(const State *s) const;
    const AdviceProposition *getAdviceProp(const State *s) const;
    const AdviceProposition *getAdviceNegProp(const State *s) const;
    set< const SimpleProposition * > getLiterals() const;
    pair< int, int > rank() const;
    bool markOwnedPreconditions(const Action *a, Ownership &o,
                                ownership w) const;
    void setUpComparisons(const ActiveCtsEffects *ace, bool rhsOpen = false);
    void resetCtsFunctions();

    ~ConjGoal() {
      for (vector< const Proposition * >::const_iterator i = gs.begin();
           i != gs.end(); ++i) {
        (*i)->destroy();
      };
    };
    void write(ostream &o) const;
  };

  class DisjGoal : public Proposition {
   private:
    const vector< const Proposition * > gs;

   public:
    DisjGoal(const disj_goal *d, const vector< const Proposition * > &g,
             const Environment &bs)
        : Proposition(bs), gs(g){};
    bool evaluate(const State *, vector< const DerivedGoal * > =
                                     vector< const DerivedGoal * >()) const;
    Intervals getIntervals(const State *s) const;
    string getPropString(const State *s) const;
    const AdviceProposition *getAdviceProp(const State *s) const;
    const AdviceProposition *getAdviceNegProp(const State *s) const;
    set< const SimpleProposition * > getLiterals() const;
    pair< int, int > rank() const;
    bool markOwnedPreconditions(const Action *a, Ownership &o,
                                ownership w) const;
    void setUpComparisons(const ActiveCtsEffects *ace, bool rhsOpen = false);
    void resetCtsFunctions();

    ~DisjGoal() {
      for (vector< const Proposition * >::const_iterator i = gs.begin();
           i != gs.end(); ++i) {
        (*i)->destroy();
      };
    };
    void write(ostream &o) const;
  };

  class ImplyGoal : public Proposition {
   private:
    const Proposition *ant;
    const Proposition *cons;

   public:
    ImplyGoal(const imply_goal *i, const Proposition *a, const Proposition *c,
              const Environment &bs)
        : Proposition(bs), ant(a), cons(c){};
    bool evaluate(const State *, vector< const DerivedGoal * > =
                                     vector< const DerivedGoal * >()) const;
    Intervals getIntervals(const State *s) const;
    string getPropString(const State *s) const;
    const AdviceProposition *getAdviceProp(const State *s) const;
    const AdviceProposition *getAdviceNegProp(const State *s) const;
    set< const SimpleProposition * > getLiterals() const;
    pair< int, int > rank() const;
    bool markOwnedPreconditions(const Action *a, Ownership &o,
                                ownership w) const;
    void setUpComparisons(const ActiveCtsEffects *ace, bool rhsOpen = false);
    void resetCtsFunctions();

    ~ImplyGoal() {
      ant->destroy();
      cons->destroy();
    };
    void write(ostream &o) const;
  };

  class NegGoal : public Proposition {
   private:
    const Proposition *p;

   public:
    NegGoal(const neg_goal *n, const Proposition *pp, const Environment &bs)
        : Proposition(bs), p(pp){};
    bool evaluate(const State *, vector< const DerivedGoal * > =
                                     vector< const DerivedGoal * >()) const;
    Intervals getIntervals(const State *s) const;
    string getPropString(const State *s) const;
    set< const SimpleProposition * > getLiterals() const;
    const AdviceProposition *getAdviceProp(const State *s) const;
    const AdviceProposition *getAdviceNegProp(const State *s) const;

    pair< int, int > rank() const;
    bool markOwnedPreconditions(const Action *a, Ownership &o,
                                ownership w) const;
    void setUpComparisons(const ActiveCtsEffects *ace, bool rhsOpen = false);
    void resetCtsFunctions();

    ~NegGoal() { p->destroy(); };
    void write(ostream &o) const;
  };

  class PreferenceGoal : public Proposition {
   private:
    const preference *pref;
    const Proposition *thePref;

    Validator *vld;

   public:
    PreferenceGoal(Validator *v, const preference *p, const Proposition *prp,
                   const Environment &bs)
        : Proposition(bs), pref(p), thePref(prp), vld(v){};
    bool evaluate(const State *, vector< const DerivedGoal * > =
                                     vector< const DerivedGoal * >()) const;
    Intervals getIntervals(const State *s) const;
    string getPropString(const State *s) const;
    set< const SimpleProposition * > getLiterals() const;
    pair< int, int > rank() const;
    bool markOwnedPreconditions(const Action *a, Ownership &o,
                                ownership w) const;
    void setUpComparisons(const ActiveCtsEffects *ace, bool rhsOpen = false);
    const AdviceProposition *getAdviceProp(const State *s) const;
    void resetCtsFunctions();
    ~PreferenceGoal() { thePref->destroy(); };
    void write(ostream &o) const;
  };

  class ConstraintGoal : public Proposition {
   private:
    const constraint_goal *constraint;
    const Proposition *trigger;
    const Proposition *requirement;

    Validator *vld;

   public:
    ConstraintGoal(Validator *v, const constraint_goal *cg,
                   const Proposition *t, const Proposition *r,
                   const Environment &bs)
        : Proposition(bs), constraint(cg), trigger(t), requirement(r), vld(v){};

    constraint_sort getCons() const { return constraint->getCons(); };
    const Proposition *getTrigger() const { return trigger; };
    const Proposition *getRequirement() const { return requirement; };
    double getFrom() const { return constraint->getFrom(); };
    double getDeadline() const { return constraint->getDeadline(); };
    void resetCtsFunctions();

    ~ConstraintGoal() {
      trigger->destroy();
      requirement->destroy();
    };
    bool evaluate(const State *, vector< const DerivedGoal * > =
                                     vector< const DerivedGoal * >()) const;
    Intervals getIntervals(const State *s) const;
    string getPropString(const State *s) const;
    set< const SimpleProposition * > getLiterals() const;
    pair< int, int > rank() const;
    bool markOwnedPreconditions(const Action *a, Ownership &o,
                                ownership w) const;
    void setUpComparisons(const ActiveCtsEffects *ace, bool rhsOpen = false);
    const AdviceProposition *getAdviceProp(const State *s) const;
    void write(ostream &o) const;
  };

  /* Problem with quantified goals: Propositions are expected to have ground
  leaves,
   * but this is obviously not true of quantified goals. Should we expand them
  out
   * here? If so, how does this impact on the environment? Presumably we have a
  local
   * environment for this case, extending the general environment?
   *

  class QfiedGoal : public Proposition {
  private:

          const qfied_goal * qfg;
          Proposition

  };

  */

  class QfiedGoal : public Proposition {
   private:
    const qfied_goal *qg;
    Environment *env;

    Validator *vld;

    // Mutable to allow single update.
    mutable Proposition *pp;

    mutable vector< const Proposition * > props;
    mutable var_symbol_list::const_iterator i;
    bool createLiterals;  // to do with evaluting qfied goals when we wish not
                          // to create literals
   public:
    QfiedGoal(Validator *v, const qfied_goal *q, const Environment &bs,
              bool b = true)
        : Proposition(bs),
          qg(q),
          env(bs.copy(v)),
          vld(v),
          pp(0),
          props(),
          i(qg->getVars()->begin()),
          createLiterals(b){};

    void create() const;

    bool evaluate(const State *s, vector< const DerivedGoal * > =
                                      vector< const DerivedGoal * >()) const;
    bool evaluateQfiedGoal(const State *s,
                           vector< const DerivedGoal * > DPs) const;
    Intervals getIntervals(const State *s) const;
    string getPropString(const State *s) const;
    set< const SimpleProposition * > getLiterals() const;
    const AdviceProposition *getAdviceProp(const State *s) const;
    const AdviceProposition *getAdviceNegProp(const State *s) const;
    pair< int, int > rank() const;
    bool markOwnedPreconditions(const Action *, Ownership &o,
                                ownership w) const;
    void setUpComparisons(const ActiveCtsEffects *ace, bool rhsOpen = false);
    void resetCtsFunctions();
    void write(ostream &o) const;
    void deletepp() const;

    ~QfiedGoal() { delete pp; };
  };

  // class TimedGoal : public Proposition still to do.
  // class SimpleGoal ?

  class Validator;

  class PropositionFactory {
   private:
    map< string, const SimpleProposition * > literals;

    Validator *vld;

    struct buildProp {
      PropositionFactory *myPF;
      const Environment &myEnv;
      bool buildNewLiterals;
      const State *state;

      buildProp(PropositionFactory *pf, const Environment &e, bool b = true,
                const State *s = 0)
          : myPF(pf), myEnv(e), buildNewLiterals(b), state(s){};
      const Proposition *operator()(const goal *g) {
        return myPF->buildProposition(g, myEnv, buildNewLiterals, state);
      };
    };

   public:
    PropositionFactory(Validator *v) : literals(), vld(v){};

    ~PropositionFactory() {
      for (map< string, const SimpleProposition * >::iterator i =
               literals.begin();
           i != literals.end(); ++i)
        delete (i->second);
    };

    const SimpleProposition *buildLiteral(const proposition *p) {
      string s(p->head->getName());
      for (parameter_symbol_list::const_iterator i = p->args->begin();
           i != p->args->end(); ++i) {
        s += " ";
        s += (*i)->getName();  //(unsigned int)(*i);
      };
      map< string, const SimpleProposition * >::const_iterator i1 =
          literals.find(s);
      if (i1 != literals.end()) return i1->second;
      const SimpleProposition *prp = literals[s] = new SimpleProposition(p);
      return prp;
    };

    const SimpleProposition *buildLiteral(const simple_effect *eff) {
      return buildLiteral(eff->prop);
    };

    const SimpleProposition *buildLiteral(const proposition *p,
                                          const Environment &bs) {
      string s(p->head->getName());
      for (parameter_symbol_list::const_iterator i = p->args->begin();
           i != p->args->end(); ++i) {
        s += " ";
        if (dynamic_cast< const var_symbol * >(*i)) {
          /*			cout << "DEBUG: " << (**i) << "\n";
                                  for(Environment::const_iterator x =
             bs.begin(); x != bs.end(); ++x)
                                          {
                                          cout << *(x->first) << " -> " <<
             *(x->second) << "\n";
                                          }
          */
          s += bs.find(dynamic_cast< const var_symbol * >(*i))
                   ->second->getName();
        } else {
          s += (*i)->getName();
        };
      };

      map< string, const SimpleProposition * >::const_iterator i1 =
          literals.find(s);
      if (i1 != literals.end()) {
        return i1->second;
      }
      const SimpleProposition *prp = literals[s] = new SimpleProposition(p, bs);
      return prp;
    };

    const SimpleProposition *buildLiteral(const simple_effect *eff,
                                          const Environment &bs) {
      return buildLiteral(eff->prop, bs);
    };

    // bool evaluate(const proposition * p,const Environment & bs,const State *
    // state) const;
    const Proposition *buildProposition(const goal *g, const Environment &bs,
                                        bool buildNewLiterals = true,
                                        const State *state = 0);
    const Proposition *buildProposition(const goal *g,
                                        bool buildNewLiterals = true,
                                        const State *state = 0);
  };

  class AdvicePropositionConj;
  class AdvicePropositionDisj;
  class AdvicePropositionLiteral;
  class AdvicePropositionDP;
  class AdvicePropositionComp;

  class APVisitor {
   public:
    virtual ~APVisitor(){};
    virtual void visitAPConj(const AdvicePropositionConj *){};
    virtual void visitAPDisj(const AdvicePropositionDisj *){};
    virtual void visitAPLiteral(const AdvicePropositionLiteral *){};
    virtual void visitAPDP(const AdvicePropositionDP *){};
    virtual void visitAPComp(const AdvicePropositionComp *){};
  };

  class AdviceProposition {
   private:
   public:
    AdviceProposition(){};
    virtual ~AdviceProposition(){};
    virtual bool isAdvice() const = 0;
    virtual void display(int indent = 0) const = 0;
    virtual void displayLaTeX(int depth = 0) const = 0;
    virtual void visit(APVisitor *apv) const {};
  };

  class AdvicePropositionConj : public AdviceProposition {
   private:
    vector< const AdviceProposition * > adviceProps;

   public:
    AdvicePropositionConj() : adviceProps(){};
    ~AdvicePropositionConj();
    bool isAdvice() const { return (adviceProps.size() > 0); };
    void addAdviceProp(const AdviceProposition *ap) {
      adviceProps.push_back(ap);
    };
    void display(int indent = 0) const;
    void displayLaTeX(int depth = 0) const;
    void visitAll(APVisitor *apv) const {
      for (vector< const AdviceProposition * >::const_iterator i =
               adviceProps.begin();
           i != adviceProps.end(); ++i) {
        (*i)->visit(apv);
      };
    };
    void visit(APVisitor *apv) const { apv->visitAPConj(this); };
  };

  class FastEnvironment;

  class AdvicePropositionDisj : public AdviceProposition {
   private:
    vector< const AdviceProposition * > adviceProps;

   public:
    AdvicePropositionDisj() : adviceProps(){};
    ~AdvicePropositionDisj();
    bool isAdvice() const { return (adviceProps.size() > 0); };
    void addAdviceProp(const AdviceProposition *ap) {
      adviceProps.push_back(ap);
    };
    void display(int indent = 0) const;
    void displayLaTeX(int depth = 0) const;

    void visitAll(APVisitor *apv) const {
      for (vector< const AdviceProposition * >::const_iterator i =
               adviceProps.begin();
           i != adviceProps.end(); ++i) {
        (*i)->visit(apv);
      };
    };
    void visit(APVisitor *apv) const { apv->visitAPDisj(this); };
  };

  class AdvicePropositionLiteral : public AdviceProposition {
   private:
    bool thereIsAdvice;
    const SimpleProposition *sp;
    bool advice;

   public:
    AdvicePropositionLiteral(bool isAd, const SimpleProposition *sp, bool a)
        : thereIsAdvice(isAd), sp(sp), advice(a){};
    ~AdvicePropositionLiteral(){};  // do not delete sp!
    bool isAdvice() const { return thereIsAdvice; };
    void changeAdvice(bool isAd, const SimpleProposition *sprop, bool a) {
      thereIsAdvice = isAd;
      sp = sprop;
      advice = a;
    };
    void display(int indent = 0) const;
    void displayLaTeX(int depth = 0) const;

    const SimpleProposition *getProp() const { return sp; };

    void visit(APVisitor *apv) const { apv->visitAPLiteral(this); };
  };

  class AdvicePropositionDP : public AdviceProposition {
   private:
    const DerivedGoal *dp;
    bool neg;

   public:
    AdvicePropositionDP(const DerivedGoal *p, bool n) : dp(p), neg(n){};
    ~AdvicePropositionDP(){};  // do not delete dp!
    bool isAdvice() const { return false; };
    void display(int indent = 0) const;
    void displayLaTeX(int depth = 0) const;
    bool isNeg() const { return neg; };
    const DerivedGoal *getDG() const { return dp; };

    void visit(APVisitor *apv) const { apv->visitAPDP(this); };
  };

  class AdvicePropositionComp : public AdviceProposition {
   private:
    bool thereIsAdvice;
    const Comparison *comp;
    string advice;
    bool neg;

   public:
    AdvicePropositionComp(bool isAd, const Comparison *c, string a, bool n)
        : thereIsAdvice(isAd), comp(c), advice(a), neg(n){};
    ~AdvicePropositionComp(){};  // do not delete comp!
    bool isAdvice() const { return thereIsAdvice; };
    void display(int indent = 0) const;
    void displayLaTeX(int depth = 0) const;
    bool isNeg() const { return neg; };
    const Comparison *getComp() const { return comp; };
    void visit(APVisitor *apv) const { apv->visitAPComp(this); };
  };

};  // namespace VAL

#endif
